Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    fib(N)  → sel(N,fib1(s(0),s(0)))
2:    fib1(X,Y)  → cons(X,n__fib1(Y,add(X,Y)))
3:    add(0,X)  → X
4:    add(s(X),Y)  → s(add(X,Y))
5:    sel(0,cons(X,XS))  → X
6:    sel(s(N),cons(X,XS))  → sel(N,activate(XS))
7:    fib1(X1,X2)  → n__fib1(X1,X2)
8:    activate(n__fib1(X1,X2))  → fib1(X1,X2)
9:    activate(X)  → X
There are 7 dependency pairs:
10:    FIB(N)  → SEL(N,fib1(s(0),s(0)))
11:    FIB(N)  → FIB1(s(0),s(0))
12:    FIB1(X,Y)  → ADD(X,Y)
13:    ADD(s(X),Y)  → ADD(X,Y)
14:    SEL(s(N),cons(X,XS))  → SEL(N,activate(XS))
15:    SEL(s(N),cons(X,XS))  → ACTIVATE(XS)
16:    ACTIVATE(n__fib1(X1,X2))  → FIB1(X1,X2)
The approximated dependency graph contains 2 SCCs: {13} and {14}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.10 seconds)   ---  May 4, 2006